T:Type, x:T, l:T List. (y:T. Dec(x = y))  Dec((x  l)) 

latex

Definitions	Dec(P), t  T, Prop, x:A. B(x), (x  l), P  Q, False, A, {T}, P  Q, True, P  Q, P & Q, P  Q
Lemmas	cons member, or functionality wrt iff, not functionality wrt iff, nil member, l member wf, not wf, false wf, decidable wf